Nuprl Lemma : sum_unroll_hi_q
11,40
postcript
pdf
i
,
j
:
.
(
i
<
j
)
(
E
:({
i
..
j
}
).
i
k
<
j
.
E
(
k
) = (
i
k
<
j
- 1.
E
(
k
) +
E
(
j
- 1))
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
+
r
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
sum
unroll
hi
origin
i, j:
.
(E:({i..j
}
). 
i 
k < j. E(k) = (i k < j - 1. E(k) + E(j - 1)) 
) i, j:.
(E:({i..j}). i k < j. E(k) = (i k < j - 1. E(k) + E(j - 1)) ) T+*>x:A. B(x)a j < b. E(j)